Model checking is an automatic technique for the verification of concurrent systems. It has several advantages over simulation, testing, and deductive reasoning, and has been used successfully in practice to verify complex sequential circuit designs and communication protocols. (See, for example, E. M. Clarke, O. Grumberg, and D. A. Peled, “Model Checking,” MIT Press, 2000; and K. L. McMillian, “Symbolic Model Checking: An Approach to the State Explosion Problem,” Kluwer Academic Publishers, 1993.)
In addition, satisfiability-based (SAT-based) bounded model checking (BMC) has been shown to be demonstrably more robust and scalable compared to methods based on binary decision diagrams (BDDs). And in sharp contrast to BDD-based methods, BMC focuses on finding bugs of bounded length—successively increasing the bound to search for longer traces.
As such, when given a design and a correctness property, BMC generates a Boolean formula by unrolling the design for k transitions such that the formula is satisfiable if and only if there is a counter-example of length k. And while BMC can find bugs in larger designs than BDD-based methods, the correctness of the property is guaranteed only for the analysis bound unless some completeness threshold is reached. (See, for example, A. Biere, A. Cimatti, E. M. Clarke, M. Fujita, and Y. Zhu, “Symbolic model checking using SAT procedures instead of BDDs,” in Proceedings of the 36th ACM/IEEE Design Automation Conference, pages 317-20, 1999; and M. Sheeran, S. Singh, and G. Stalmarck, “Checking safety properties using induction and a SAT solver,” in Conference on Formal Methods in Computer-Aided Design, Vol. 1954 of Lecture Notes in Computer Science, pages 108-25, Springer, November 2000.)
The use of SAT-based quantifier elimination through a series of SAT calls has been the focus of Symbolic Model Checking algorithm(s) (a.k.a. Unbounded Model Checking (UMC)) proposed in the prior art. See A. Gupta, Z. Yang, P. Ashar, “SAT-based Image Computation with Applications in Reachability Analysis,” in Proceedings of Conference on Formal Methods in Computer-Aided Design, pp. 354-71 (2000); H. J. Kang and I. C. Park, “SAT-based Unbounded Symbolic Model Checking,” in Design Automation Conference, pp. 840-43 (2003); K. McMillan, “Applying SAT Methods in Unbounded Symbolic Model Checking,” in Computer-Aided Verification, pp. 250-64 (2002). In these approaches, the transition relation is represented in conjunctive normal form (CNF) and a SAT procedure is used to enumerate all state cube solutions. Similar to traditional model checking, the number of pre-image computations required is bounded by the diameter of the state space, and the method provides a guarantee of correctness when the safety property is true.
In one approach in the prior art, a blocking clause representing the negation of the enumerated state cube is added at each step. In another approach, a redrawing of the implication graph is carried out to enlarge the state cube. Additionally, a two-level minimizer has been used to compact the increase in CNF size due to the addition of new blocking clauses.
Note that in both approaches, only a single state cube is captured at any enumeration step. Since the number of required enumerations is bounded below by the size of a two-level prime and irredundant cover of the entire state set, quantifier elimination based on cube-by-cube enumeration tends to be expensive.
In a slightly different approach in the prior art, SAT-based quantifier elimination is achieved using a PODEM-based ATPG solver. (See, for example S. Sheng and M. Hsiao, “Efficient Pre-image Computation Using a Novel Success-Driven ATPG,” in Design Automation and Test in Europe (2003).) The approach described therein uses a satisfying cutset to prune the search space for new solutions and a BDD representation for the enumerated solutions. And while this approach does reduce the umber of backtracks due to efficient pruning, it still has to enumerate all state cubes and is prone to the BDD explosion problem.
In yet another approach, ATPG is used as the search engine, and state cube enlargement is achieved using a separate justification procedure once a satisfying SAT result is found. (See, for example, M. K. Iyer, G. Parthasarathy, and K. T. Cheng, “SATORI: An Efficient Sequential SAT Solver for Circuits,” in International Conference on Computer-Aided Design (2003).) Unfortunately, however, this approach is also limited by its cube-wise enumeration strategy.
In yet another approach, the transition relation is expressed in CNF while the enumerated states are represented as one or more BDDs. (See A. Gupta et al., cited above.) With this approach, the image computation is performed by invoking BDD-based quantification on the CNF formula at intermediate points in the SAT decision tree. Bounding against the already enumerated BDDs provides additional pruning of the SAT search as well as a means to detect the fix point. While this method does try to enumerate more than one cube in every SAT enumeration, its drawback is that it is based on BDDs, and therefore not scalable or robust.
In still another approach of SAT-based UMC, interpolants are derived from the refutation generated by a SAT solver on unsatisfiable instances, instead of SAT-based quantifier elimination. See K. McMillan, “Interpolation and SAT-based Model Checking,” in Computer-Aided Verification, pp. 1-13 (2003). However, the approach computes only approximate reachable states while it would be preferable to compute exact reachable states.